/******************************************************************************

    Copyright (C) 2006 Alessio Stalla (alessiostalla@gmail.com)

    This file is part of PrettyProlog.

    PrettyProlog is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    PrettyProlog is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with PrettyProlog; if not, write to the Free Software
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA

    See the file COPYING for further details.

 *****************************************************************************/

package prettyprolog.engine;

import java.io.Serializable;
import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;
import java.util.Vector;

import prettyprolog.datatypes.Callable;
import prettyprolog.datatypes.Constraint;
import prettyprolog.datatypes.Substitution;
import prettyprolog.datatypes.Symbol;
import prettyprolog.datatypes.Term;
import prettyprolog.datatypes.Variable;

/**
 * A Clause is a rule in a Theory. Clauses have an head and a body; both are
 * {@link prettyprolog.datatypes.Callable Callable}s, but the head must have a
 * non-null symbol, while the body is a tuple of
 * {@link prettyprolog.datatypes.Callable Callable}s and
 * {@link prettyprolog.datatypes.Variable Variable}s so its symbol is always
 * null.<br />
 * The engine solves a goal G by finding a clause whose head unifies with a
 * subgoal of G, and replacing this subgoal with the clause's body, thus
 * obtaining new goals and so on, until an empty goal is obtained or no unifying
 * clauses are found.<br />
 * The head can also be null, and in that case the Clause is a directive, a special
 * object that is executed as soon as it is asserted in a Theory. Such clauses do not
 * participate in goal solving (since their null head does not unify with anything);
 * rather, they are used to perform side-effects on the Prolog engine, for example declaring
 * that a particular symbol names a system predicate.
 */
public class Clause implements Serializable {

	private static final long serialVersionUID = 1L;
	
	protected Callable head;
	protected Callable body;
	protected Callable clause;
	protected Constraint constr;

	/** Creates a new Clause with null head and body. */
	protected Clause() {
	}

	public Clause(Symbol clauseSymbol, Callable head, Callable body, Constraint constr) {
		this.head = head;
		this.body = body;
		this.constr = constr;
		initClause(clauseSymbol);
	}

	/**
	 * Constructs a new Clause using a Callable.
	 * 
	 * @param c
	 *            the Callable passed to this constructor; it is interpreted as
	 *            follows:
	 *            <ul>
	 *            <li>If its Symbol is ':-', the first argument is used as the
	 *            clause's head, the rest are used to construct the body. The
	 *            head must be a Callable, and the body can only contain
	 *            Callables or Variables; a NotAClauseException is thrown if
	 *            these conditions aren't met.</li>
	 *            <li>Else, c becomes the clause's head and the body is
	 *            initialized to an empty tuple.</li>
	 *            </ul>
	 * @param clauseSymbol
	 *            the symbol used as a clause marker, <code>:-</code>. Passed as
	 *            an argument so that Clause needs not to refer to a symbol
	 *            table.
	 */
	public Clause(Callable c, Symbol clauseSymbol) throws NotAClauseException {
		if (c == null) {
			throw new NotAClauseException(null);
		}
		Symbol sym = c.getSymbol();
		List<Term> args = c.getArgs();
		if (sym != null) {
			if (sym.equals(clauseSymbol)) {
				if (args.size() > 0 && args.get(0) instanceof Callable) {
					head = (Callable) args.get(0);
					constr = new Constraint (new Vector<Term>());
					List<Term> temp = head.getArgs();
					List<Term> sub = args.subList(1, c.getArgCount());
					if (!makeBody(sub)) {
						throw new NotAClauseException(c);
					}
				} else {
					throw new NotAClauseException(c);
				}
			} else {
				head = c;
				body = new Callable(null, new Vector<Term>());
				constr = new Constraint(new Vector<Term>());
				List<Term> temp = head.getArgs();
			}
		} else {
			throw new NotAClauseException(c);
		}
		initClause(clauseSymbol);
	}
	
	protected void initClause(Symbol clauseSymbol) {
		List<Term> args = new ArrayList<Term>();
		args.add(head);
		args.addAll(body.getArgs());
		clause = new Callable(clauseSymbol, args);
	}

	/**
	 * Constructs a new Clause.
	 * 
	 * @param c
	 *            the clause's head.
	 * @param ls
	 *            the clause's body; it must contain only
	 *            {@link prettyprolog.datatypes.Callable Callable}s and
	 *            {@link prettyprolog.datatypes.Variable Variable}s.
	 */
	public Clause(Callable c, List<Term> ls) throws NotAClauseException {
		head = c;
		if (!makeBody(ls))
			throw new NotAClauseException();
	}

	private boolean makeBody(List<Term> ls) {
		List<Term> body_args = new Vector<Term>();
		List<Term> cons_args = new Vector<Term>();
		for(Term t : ls) {
			if (t instanceof Callable) {
				// body_args.add(t);	
				List<Term> temp = ((Callable) t).getArgs();
				Symbol sy = (Symbol) ((Callable) t).getSymbol();
				
				if (!((sy.toString().equals("#>")) ||
				      (sy.toString().equals("#>=")) ||
				      (sy.toString().equals("#<")) ||
				      (sy.toString().equals("#=<")) ||
				      (sy.toString().equals("#\\=")) ||
				      (sy.toString().equals("=")) ||
				      (sy.toString().equals("#=")))) {
//				      (sy.toString().equals("dom")))) {	
					  body_args.add(t);
				} else {
					cons_args.add(t);
					if (!((sy.toString().equals("domain")))) {
						body_args.add(t);
					}
				}
			} else if (t instanceof Variable) {
				body_args.add(t);
			} else
				return false;
		}

		body = new Callable(null, body_args);
		constr = new Constraint(cons_args);
		return true;
	}

	/** @return the head. */
	public Callable getHead() {
		return head;
	}

	/**
	 * @return the tuple of Callables and/or Variables that make up the body of
	 *         this Clause. WARNING: it is an error to destructively modify the
	 *         return value.
	 */
	public Callable getBody() {
		return body;
	}
	
	public Constraint getConstr() {
		return constr;
	}

	public String toString() {
		String bodystr = "";
		String constrStr = "";
		List<Term> body = this.body.getArgs();
		List<Term> cons = this.constr.getCons();
		int size = body.size();
		int c_size = cons.size();
		for (int i = 0; i < size - 1; i++) {
			bodystr += body.get(i) + ", ";
		}
		if (size > 0) {
			bodystr += body.get(size - 1);
		}
		
		for(int i = 0; i < c_size - 1; i++)
		    constrStr += cons.get(i) + ", ";
	    if(c_size > 0)
		constrStr += cons.get(c_size - 1);	
	    
		if(head == null) {
			if (constrStr.equals("")) {
				return ":- " + bodystr + ".";
			} else {
				return ":- " /* + constrStr +" , "+ " || "+*/ +bodystr + ".";
			}
		} else if (!bodystr.equals("")) {
			if (constrStr.equals("")) {
				return head + " :- " + bodystr + ".";
			} else {
				return head + " :- " /*+ constrStr +" , "+ " || "+*/+ bodystr + ".";
			}
		} else {
			if (!constrStr.equals("")) {
				return head + " :- "/* + constrStr*/ + ".";
			} else 
			return head + ".";
		}
	}

	/**
	 * Creates a copy of this clause. All the variables in the head and body are
	 * renamed to avoid name clashes.
	 */
	public Clause copy() {
		Clause copy = new Clause();
		Substitution vars = new Substitution();
		copy.head = head != null ? (Callable) head.copy(vars) : null;
		List<Term> copy_body = new LinkedList<Term>();
		List<Term> copy_cons = new LinkedList<Term>();
		for (Term t : constr.getCons()) {
			if(t instanceof Callable) {
//				if (!((Callable) t).getSymbol().toString().equals("domain")) {
					copy_cons.add(t.copy(vars));
//				}
			}
		}
		for (Term t : body.getArgs()) {
			copy_body.add(t.copy(vars));
		}
		copy.constr = new Constraint(copy_cons);
		copy.body = new Callable(null, copy_body);
		return copy;
	}
	
	public Callable asCallable() {
		return clause;
	}
	
	public boolean isDirective() {
		return head == null;
	}

}